i1, i2, j1, j2:. (i1  j1)  (i2  j2 )  ((i1 - i2)  (j1 - j2)) 

latex

Up	int 2, int 2
Definitions	t  T, P  Q, x:A. B(x), True, T, False, A, , i  j , A  B
Lemmas	le wf, ge wf, true wf, squash wf, minus functionality wrt le, add functionality wrt le